Trait isotope::ctx::eval::ReductionConfig [−][src]
pub trait ReductionConfig { type AsRef: ReductionConfig; fn register_push_subst(&mut self, subst: &TermId) -> Result<(), Error>; fn register_pop_subst(&mut self) -> Result<(), Error>; fn register_beta(&mut self) -> Result<(), Error>; fn register_eta(&mut self) -> Result<(), Error>; fn eta(
&self,
term: &Term,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<bool, Error>; fn sub(
&self,
term: &Term,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<bool, Error>; fn head(
&self,
term: &Term,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<bool, Error>; fn intersects(&self, filter: VarFilter, code: Code, form: Form) -> bool; fn as_ref_mut(&mut self) -> &mut Self::AsRef; }
Expand description
A reduction configuration
Associated Types
type AsRef: ReductionConfig
[src]
type AsRef: ReductionConfig
[src]Get this reduction configuration as a reference
Required methods
Register a pushed substitution.
fn register_pop_subst(&mut self) -> Result<(), Error>
[src]
fn register_pop_subst(&mut self) -> Result<(), Error>
[src]Register a popped substitution.
fn register_beta(&mut self) -> Result<(), Error>
[src]
fn register_beta(&mut self) -> Result<(), Error>
[src]Register a beta reduction: return whether to terminate beta reduction (Error::StopReduction
)
fn register_eta(&mut self) -> Result<(), Error>
[src]
fn register_eta(&mut self) -> Result<(), Error>
[src]Register an eta reduction: return whether to terminate eta reduction (Error::StopReduction
)
Given a term, whether to attempt an eta reduction or terminate (Error::StopReduction
)
Given a term, whether to attempt a subterm reduction or terminate (Error::StopReduction
)
Given a term, whether to attempt a head reduction or terminate (Error::StopReduction
)
Get whether a term with the given filter intersects with this context
fn as_ref_mut(&mut self) -> &mut Self::AsRef
[src]
fn as_ref_mut(&mut self) -> &mut Self::AsRef
[src]Get this reduction configuration as a mutable reference